\begin{tabbing}
$\forall$\=${\it poss}$:(ES\{i\}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$), $T$:Type$_{\mbox{\scriptsize i}}$, $s$:$T$, $i$:Id, $P$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$),\+
\\[0ex]$R$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$), ${\it Rs}$:($T$$\rightarrow$$T$$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).
\-\\[0ex](EquivRel $1$,$2$:possible{-}event\{i:l\}(${\it poss}$). $R$($1$,$2$))
\\[0ex]$\Rightarrow$ (\=$\forall$$e$, ${\it e'}$:possible{-}event\{i:l\}(${\it poss}$).\+
\\[0ex]poss{-}consistent($i$;$T$;$s$;$e$;${\it Rs}$) $\Rightarrow$ poss{-}consistent($i$;$T$;$s$;${\it e'}$;${\it Rs}$) $\Rightarrow$ $R$($e$,${\it e'}$))
\-\\[0ex]$\Rightarrow$ $\neg$ma{-}knows\=\{i:l\}\+
\\[0ex](${\it poss}$; $i$; $T$; $s$; $P$; ${\it Rs}$; $R$)
\-\\[0ex]$\Rightarrow$ ma{-}knows\=\{i:l\}\+
\\[0ex](${\it poss}$; $i$; $T$; $s$; ($\lambda$$e$.$\neg$es{-}knows\{i:l\}(${\it poss}$; $R$; $P$; $e$)); ${\it Rs}$; $R$)
\-
\end{tabbing}